{-# LANGUAGE TypeFamilies, TypeOperators, MultiParamTypeClasses,
  FlexibleContexts, FlexibleInstances, UndecidableInstances,
  ScopedTypeVariables  #-}

{-# OPTIONS_GHC -fcontext-stack=250 #-}

module CnvExample2A (Cnv, Idiom, Convert(..)) where

import TypeBasics
import Yoko



import Control.Applicative




type instance Cnv cnv (DCsOf t sum) = Cnv cnv t
instance ConvertSumTo cnv sum (Cnv cnv t) => Convert cnv (DCsOf t sum) where
  convert cnv = convertSumTo cnv . unDCsOf




type family Cnv cnv a
type family Idiom cnv :: * -> *
class Applicative (Idiom cnv) => Convert cnv a where
  convert :: cnv -> a -> Idiom cnv (Cnv cnv a)




class Applicative (Idiom cnv) => ConvertSumTo cnv sum t where
  convertSumTo :: cnv -> sum -> Idiom cnv t

instance (ConvertSumTo cnv a t, ConvertSumTo cnv b t
         ) => ConvertSumTo cnv (a :+: b) t where
  convertSumTo cnv = foldPlus (convertSumTo cnv) (convertSumTo cnv)

-- NB only works if there's exactly one matching constructor
instance (Generic dc, Just (N dc') ~ FindDCs (Tag dc) (DCs t),
          ConvertRs cnv (Rep dc), Rep dc' ~ RsConvert cnv (Rep dc),
          DC dc', Range dc' ~ t, DT t
         ) => ConvertSumTo cnv (N dc) t where
  convertSumTo cnv = 
    foldN $ liftA (rejoin . (id :: dc' -> dc') . obj) . convertRs cnv . rep



type family FindDCs s sum
type instance FindDCs s (N dc) =
  If (Equal s (Tag dc)) (Just (N dc)) Nothing
type instance FindDCs s (a :+: b) = DistMaybePlus (FindDCs s a) (FindDCs s b)




-- applies cnv to every Rec in a product; identity on other factors
type family RsConvert cnv prod
class Applicative (Idiom cnv) => ConvertRs cnv prod where
  convertRs :: cnv -> prod -> Idiom cnv (RsConvert cnv prod)

type instance RsConvert cnv (Rec a) = Rec (Cnv cnv a)
instance Convert cnv a => ConvertRs cnv (Rec a) where
  convertRs cnv (Rec x) = Rec <$> convert cnv x

type instance RsConvert cnv (Dep a) = Dep a
type instance RsConvert cnv U     = U
instance Applicative (Idiom cnv) => ConvertRs cnv (Dep a) where convertRs _ = pure
instance Applicative (Idiom cnv) => ConvertRs cnv U     where convertRs _ = pure

type instance RsConvert cnv (a :*: b) = RsConvert cnv a :*: RsConvert cnv b
instance (ConvertRs cnv a, ConvertRs cnv b) => ConvertRs cnv (a :*: b) where
  convertRs cnv (a :*: b) =
    (:*:) <$> convertRs cnv a <*> convertRs cnv b
